A simple language has  been devised for more precise  descriptions of

strategies than Boolean combinations of the builtin strategies.  This

language is also useful for describing patterns for  searching clause

lists using FIND and FINDC.

This  language allows  rather  arbitrary functions  on  the syntactic

structure of  clauses terms  and literal.  It  is also  expandable to

handle semantic characterizations.

The  legal variables are of three sorts: clauses literals  and terms.

The interpretation of  the constructed formulas differs  depending on

whether the formula is an  editing strategy, a choice strategy,  or a

pattern.  Formulas  to be used for choice strategies are  supposed to

be applied to a binary rule  of inference, I, in the presence  of two

clauses, C1 and C2;  that is, I(C1,C2).  An editing  strategy formula

is to be applied to a single clause, thus there should be exactly one

`clause  variable',  currently named  C.   Thus when  we  give choice

strategies then formula is used  as a filter on each  candidate; when

we use the formulas on clause-lists in the editing phase, they are to

be `mapcar'ed .

Literal  and  term   variables  are  designated   by  l1,l2,l3,...and

t1,t2,t3,....

All quantifiers are implicitly relativized. E.g.  ∀l1∃t2... means for

every  literal in  the current  clause  there is  a term  in  l1 such

that...

PRIMITIVES:



1) ancestry     TR(x)

If x is clause  c, then TR(x) gives the  ancestry.  If x is  either a

literal or a term --l or t-- then TR(x) gives the structure of x.

Examples:

If x is  an initial clauses  then TR(x) is NIL.  If x is  a deduction

then TR  gives a   list of  the clauses  appearing in  the derivation

tree.

2) length               α(x)

If  x  is  a  clause then  α(x)  gives  the  usual  length--number of

literals.  If x is  a literal or term  then α(x) gives the  number of

symbols which appear

Examples:

α(c)=1 is true if c is a unit-clause.

3) depth                ∂(x)

If x is a clause, then  ∂(x) gives the depth of the  derivation tree.

If x  is a literal  or term  then ∂(x) gives  the depth  of function-

nesting.

PREDICATES:

=,<,>,≠,¬       equality,less-than,greater-than,not-equal, not
∧,∨,ε           and,or,clever membership.
[ p→e; ...]     conditionals


Examples: a) ∂(t1)<5 ∧TR(c)=NIL

Depth of nesting is less than 5 and clause is initial.

b) [α(c)=1 → ∀l1 E(_,_)εTR(l1) ; T → ∀l1 ¬ -εTR(l1)]



   If clause  is unit  the the predicate,  E, must  appear; otherwise

every literal    in c must be positive.

MATCHING:

+,-             sign of a literal ⊂,⊃             set  delimiters for

and-membership ⊃,⊂             set delimiters for or-membershit

Examples; ⊂2,3,4⊃εTR(c)

   Each clause 2,3,and 4 must appear in the tree of c.

⊃2,3,4⊂εTR(c)

   At least one of these clauses must appeaar.

_               matches any term

x,y,z,u,v       used to match sub-terms.

Examples: f(_,_) matches any occurrence of the function-letter,f.

f(g(x,_),_,x)  matches  any  occurrence  of  f  such  that  f's first

position is an  occurrence of g; and  g's first position  matches the

third position of f.

Examples:

Definition of some of the builtin strategies in the language.

ANCESTRY:       TR(C1)=NIL ∨ TR(C2)=NIL ∨ C2εTR(C1) ∨ C1εTR(C2)
SUPPORT[...]:   [TR(C2)=NIL → ⊃...⊂εTR(C2);T → T]
UNIT:           α(C1)=1 ∨ α(C2)=1
VINE:           TR(C1)=NIL ∨ TR(C2)=1

LENGTH[#]:      α(C) > # 
DEPTH[#]:       ∂(C) > #